ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), l:IdLnk, tgs:(Id List), ks:(Knd List),
g:(k:{k:Knd| (k  ks)} (tg:{tg:Id| (tg  tgs)} 
g:( (decl-state(ds)ma-valtype(da; k)(fpf-cap(da; Kind-deq; rcv(l,tg); void) List))) List).
no_repeats(Id; tgs)
 l_all(tgs; Id; tg.(fpf-dom(Kind-deq; rcv(l,tg); da)))
 (es:event_system{i:l}. 
 (l_all(ks; Knd; k.sends-p(es; ds; k; fpf-cap(da; Kind-deq; k; void); l; es-dt(l; da); (g(k))))
  l_all(tgs; Id; tg.sframe-p(es; l; tg; ks)))
  es-decls(es;source(l);ds;da)
  with decls ds 
  with decls da
  sends on l from e 
  include if deq-member(Kind-deq; es-kind(es; e); ks)
  include then tagged-list-messages(es-state-when(es; e); es-val(es; e); (g(es-kind(es; e))))
  include else []
  include fi  
  and only these for tags in tgs) 

latex

Definitions

x:A. B(x), P  Q, t  T, prop{i:l}, x. t(x), with decls ds dasends on l from e include f(e) and only these for tags in tgs, P  Q, A c B, x:A. B(x), T, True, P  Q, P  Q, subtype(S; T), top, t.1, compose(f; g), decl-state(ds), sends-msgs(s; v; tg_f), es-state(es; i), ma-valtype(da; k), P  Q, fpf-cap(f; eq; x; z), guard(T), if b then t else f fi , tt, ff, alle-at(es; i; e.P(e)), ||as||, Y, sq_type(T), A  B, A, False, (x  l), int_seg(i; j), lelt(i; j; k), l_all(L; T; x.P(x)), suptype(S; T), x(s), sframe-p(es; l; tg; L), sends-p(es; ds; k; T; l; dt; g), es-rcv-from(es; e; l; L), SqStable(P), Knd, , Unit, , Id, tagged-list-messages(s; v; L), t.2,

Lemmas

event system wf, l all wf, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, rcv wf, no repeats wf, l member wf, decl-state wf, ma-valtype wf, fpf-cap wf, Id wf, IdLnk wf, fpf wf, Knd wf, es-decls wf, lsrc wf, es-decls-iff, es-E wf, es-isrcv wf, es-lnk wf, es-tag wf, es-sender wf, es-rcv-kind, squash wf, true wf, es-kind wf, es-loc wf, ldst wf, es-loc-sender, id-deq wf, es-dt wf, top wf, map-map, subtype rel list, implies functionality wrt iff, map wf, member map, l member set, list-set-type-property, decidable assert, sq stable from decidable, pi1 wf, concat wf, subtype rel self, deq wf, es-state-when wf, subtype rel dep function, es-vartype wf, list-set-type-member, decidable l member, decidable equal Id, subtype rel transitivity, es-valtype wf, bool wf, eqtt to assert, fpf-ap wf, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, Knd sq, deq-member wf, assert-deq-member, not functionality wrt iff, int seg wf, es-val wf, length wf1, tagged-list-messages wf, length-map, es-rcv-from-implies, es-index wf, es-Msgl wf, es-sends wf, select wf, map select, le wf, member-concat, es-dt-cap, pi2 wf, Id sq, es-rcv-from-member-index, es-dt-dom, sends-p wf, fpf-cap-void-subtype